2021年度後期哲学演習I 直観主義論理のメモ
#直観主義論理
https://www.youtube.com/watch?v=_9eglEQy2zY&list=PL54C_zUEsyCahh7TYscJWwBEtVNHIrtOU&index=5
証明 = 構成
古典論理には非構成的なトリックが存在する
背理法はどうなんだ？
例.存在しないを仮定し，これを否定して存在するを主張する
二重否定除去を否定する
https://www.youtube.com/watch?v=hCvU8KEsPmU&list=PL54C_zUEsyCahh7TYscJWwBEtVNHIrtOU&index=6
前順序を$ \leqで表す
直観主義論理のフレーム
空でない集合$ Wと，その上の前順序$ \leqからなる順序対$ \lang W,\leq \rang
様相論理S4のフレームと同じである
直観主義論理のモデル
直観主義論理のフレーム$ \lang W,\leq \rang
$ Wの各要素，各命題変項の対に対しての関数$ vが次の性質を満たす
遺伝性(直観主義論理)
$ v(x,p) = 1かつ$ x \leq yならば，$ v(y,p) = 1
$ vを付値と言って，フレームと付値の対$ \lang W,\leq,v \rangを直観主義論理のモデルと呼ぶ
理想的数学者
https://gyazo.com/1413c2d69e1ccf893f0742bd90f45047
直観主義論理の$ \to,\lnotは少し意味が違う
https://gyazo.com/62ff694fcebec8e579fa7829614c40cc
https://gyazo.com/448adc219e31ceec8567eaa0f6e0477d
直観主義の含意は厳密含意に似ている
$ v(x,A\to B)=1の意味
$ Aの証明さえあれば$ Bの証明を構成できる方法がありますよ
関連: Brouwer-Heyting-Kolmogorov解釈
$ v(x,\lnot A) = 1の意味
時点（世界）$ xにおいて$ Aは証明不可能であるという証明がある
ここから，$ v(x,\lnot A) = 1から$ v(x,\lnot A) = 0は成り立たないことが示される
直観主義論理での否定の扱われ方
https://www.youtube.com/watch?v=emYsnYFe5Z0&list=PL54C_zUEsyCahh7TYscJWwBEtVNHIrtOU&index=7
遺伝性(直観主義論理)は拡張される
命題変項$ pだけでなく，任意の論理式$ Aについても遺伝性へと拡張される
$ v(x,A) = 1かつ$ x \leq yなら$ v(y,A)=1
論理式の構成に関する帰納法
性質$ \phiについて
1. 最も単純な論理式である命題変項$ pで$ \phi成り立つこと
2. 論理式$ A,Bが$ \phiを満たすと仮定し
$ A \lor B,A\land B,A\to B,\lnot Aでも$ \phiが満たされること
1,2を満たすなら，任意の論理式で性質$ \phiが成り立つことが証明出来る
証明，論理式の構成に関する帰納法を用いる
1については自明
2
$ A\land Bの場合
主張
$ v(x,A\land B) = 1かつ$ x \leq yなら$ v(y,A\land B)=1
$ v(x,A \land B)=1,x\leq yとする
演算子の定義より，$ v(x,A)=1,v(x,B)=1である
仮定より，$ v(y,A)=1,v(y,B)=1である
演算子の定義より，$ v(y,A\land B) = 1である，証明終了
$ A\lor Bの場合
$ A\land Bの場合と同様なので省略
$ \lnot Aの場合
主張
$ v(x,\lnot A) = 1かつ$ x \leq yなら$ v(y,\lnot A)=1
$ v(y,\lnot A)=1$ \iff$ x\leq yなる全ての$ yについて$ v(y,A)=0
$ v(x,\lnot A)=1,x\leq yとする
演算子の定義より
$ x\leq zとなる全ての$ zで$ v(z,A) = 0である
このとき$ y,zは同じものであると考えられる…？
SnO2WMaN.iconわからないな，もしかして自明に成り立つのかこれ
$ A \to Bの場合
$ \lnot Aの場合とまあ近いことにはなると思う
https://www.youtube.com/watch?v=7PGBSWaey5Q&list=PL54C_zUEsyCahh7TYscJWwBEtVNHIrtOU&index=8
直観主義論理の反例モデル
直観主義論理のモデル$ M = \lang W,\leq,v \rang
ある$ x \in Wについて
$ B \in Xで$ v(x,B)=1
$ v(x,A)=0
が成り立つなら，$ Mを前提$ Xから結論$ Aへの推論への反例モデルと呼ぶ
フレームの妥当性
フレーム$ F=\lang W,\leq \rangで前提$ Xから結論$ Aへの推論の反例モデルが作れないなら
直観主義論理のフレームにおいて妥当である
$ X \models^F Aと書く
全てのフレーム$ Fで$ X \models^F Aならその推論は
直観主義論理において妥当である
$ X \models_{Int} Aあるいは単に$ X \models Aと書く
直観主義論理では排中律が成り立たない
$ \not\models A \lor \lnot A
$ x\leq y
$ v(x,p)=0, v(y,p)=1を考えると，
$ v(x, \lnot p) = 0である
ここから，$ v(x,p\lor \lnot p) = 0が成り立つ
以下，直観主義論理で妥当だったり非妥当だったりする推論
$ A \models \lnot\lnot A二重否定導入
$ \lnot\lnot A \not\models A二重否定除去
$ A\lor B,\lnot B \models A選言三段論法
$ (A\land B) \to C \not\models (A \to C)\lor(B \to C)
$ A \to B \models \lnot B \to \lnot A対偶の導入
$ \lnot B \to \lnot A \models A \to B対偶の除去
https://www.youtube.com/watch?v=g9d_vECcSTg&list=PL54C_zUEsyCahh7TYscJWwBEtVNHIrtOU&index=9
直観主義論理では排中律が成り立たない
$ \not\models_{Int} A \lor \lnot A
$ Aか$ Aでないかのどちらかとは限らない
どういうことなのか？
Kurt Gödel
直観主義論理は有限多値論理ではないことが証明された
直観主義論理
「$ Aが真」とは「Aの証明が存在すること」
「$ Aが偽」なら「$ \lnot Aが真/の証明が存在すること」
直観主義論理では排中律が成り立たない
「肯定か否定が，いつか証明される可能性がある，しかしまだ証明されていない」という状態がある
「まだ真とも偽とも言えない」命題がある
https://gyazo.com/8f65897f0fafb30354afec0f3255d2c1
https://gyazo.com/32371133b764564a942fdf16612d0746
計算複雑性理論
直観主義論理は「原理的には可能」に位置する
https://www.youtube.com/watch?v=wBlUPOpD0PA&list=PL54C_zUEsyCahh7TYscJWwBEtVNHIrtOU&index=10
直観主義論理は有限多値論理の一種ではない
補題：直観主義論理の選言特性
$ \models_{Int} A \lor Bならば，$ \models_{Int}Aまたは$ \models_{Int}Bのどちらかが成り立つ
証明
$ \not\models Aかつ$ \not\models Bのそれぞれの反例モデルを合体させると$ \not\models A \lor Bの反例モデルが作れる
対偶を取って証明
命題：直観主義論理は3値論理/有限多値論理では無い
https://gyazo.com/f328d72542cb8f7ef508074f6fd97d9c
https://gyazo.com/9a16bc61f751b30dcf127b845755c82a
鳩の巣原理
以上の議論を$ n値論理なら命題変項を$ n+1個の命題変項を用意する
https://www.youtube.com/watch?v=JAxIgTfMe7I&list=PL54C_zUEsyCahh7TYscJWwBEtVNHIrtOU&index=12
Glivenkoの定理
古典論理を直観主義論理へ埋め込む
任意の論理式$ Aについて，
$ \models_{CL} A \iff \models_{Int} A
$ \models_{CL}を古典論理で妥当
$ \models_{Int}を直観主義論理で妥当
https://gyazo.com/b48ba980e80055464c77ee873a7c4fbe
Gödel変換
直観主義論理を様相論理S4へ埋め込む
フレームがいずれも前順序であることを利用
https://gyazo.com/f84ed1be7a6889f7eda18e2bc6b1d5aa
様相論理側の$ \toは実質含意である
$ \tau(A \to B) = \Box (\tau(A) \to \tau (B)) = \tau(A) \Rightarrow \tau(B)
厳密含意
https://gyazo.com/c53e1c76d23bc8facf55452ae17bf434
証明
$ \not\models_{S4} \tau(A) \implies \not\models_{Int} A
様相論理S4の反例モデルを直観主義論理の反例モデルに変換
遺伝性(直観主義論理)のズレを補正
https://gyazo.com/3db6ed5318d3fd2c39c87cb540981ea1
$ \not\models_{Int} A\implies \not\models_{S4} \tau(A)
https://gyazo.com/83a1de1fa7b0f24c4b7bfd4833ee068f
$ \tau(A)と$ \Box\tau(A)が同値
直観主義論理にから持ってきた命題は真ならば必然的に真であるになる
数学的命題とか
https://gyazo.com/46c9b0a55cea62800a5b0363b30bafd5